Design: Error-Lang as a Trope IR front end (trope-particularity integration)#25
Merged
Merged
Conversation
The three "Safety Proofs" in src/abi/Foreign.idr (stabilityBounded,
positionalDeterministic, paradoxMonotonic) were not proofs: each fabricated
its evidence with cast ()/cast Refl over an IO action. Replace them with
genuine, self-contained Idris2 modules, machine-checked under Idris 2 v0.8.0
(no believe_me / assert_total / cast / postulate):
- Stability.idr : stability score is bounded in [0,100] (clamp model of
compiler/src/Types.res calculateStability).
- Positional.idr : positional-operator behaviour is deterministic over the
pure model of the Zig FFI (a genuine Refl, not IO cast Refl).
- Paradox.idr : the two threshold-gated factors are monotone; the blanket
"paradox detection monotonic" claim is RETRACTED -- proving
it honestly surfaced that scope_leakage is prime-gated and
therefore non-monotone (line 7 prime, line 8 not).
Foreign.idr is reduced to an honest, self-contained ABI binding layer.
Add error-lang-abi.ipkg and verification/check-proofs.sh (idris2 --check all
four modules). Rewrite PROOF-NEEDS.md to record what is proved, what is
retracted, the toolchain, and open conformance obligations.
The language's satirical "100% production-ready / formally verified"
self-presentation in README/WHITEPAPER is intentional and left intact; this
change only makes the underlying proof artifacts real and honest.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
…integration) Adds docs/Trope-Particularity-Integration.adoc — a design (not yet implemented) for lowering Error-Lang's Echo operations and stability factors to the language-neutral Trope IR (hyperpolymath/trope-checker, v0.1 prevent profile) and consuming the verified verdict + witness. - Object/effect/grade correspondence: Echo<A,B> <-> Trope[Phi], EchoR <-> FloatingQuality, echo/echo_to_residue/echo_input/echo_output <-> preserve/ detach/project. echo_to_residue IS detach (bond=Severed, irrecoverable), matching the [Stab-Erase] debit and "decomposition must be visible". - stabilityFactor -> grade mapping; the silent instabilities (GlobalState, RaceCondition) land on the deceptive Conflated bottom -> a lowering fault under the prevent profile. - Verdict mapping: scalar calculateStability -> use-model floor + p-sufficient/ p-insufficient + witness edge (the invariant-path argmin Stability.idr already reasons about). - Architecture (reference, never vendor; schema is the trust boundary), the per-front-end O2 lowering-correctness obligations (L-Echo/L-Grade/L-Silent/ L-Floor), and a 4-phase plan. Builds on docs/Echo-Decomposition.adoc; references echo-types, trope-checker and trope-particularity-workbench by URL only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
Hypatia structural_drift flagged `src/idris2/` and `src/aggregate/` in the trope-integration design as dangling references "surviving a directory rename". Both are deliberately *external*: the trope-checker repo's Idris2 core and the panic-attack repo's aggregate module. Reword as unambiguously external (drop the bare `src/<dir>/` form) so the heuristic no longer reads them as internal error-lang tree paths. No substantive content change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
hyperpolymath
marked this pull request as ready for review
June 23, 2026 21:10
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What & why
Adds one design document —
docs/Trope-Particularity-Integration.adoc— proposing that Error-Lang become a second front end to the portable trope-checker (hyperpolymath/trope-checker): lowering its Echo operations and stability factors to the language-neutral Trope IR (v0.1,preventprofile) and consuming the verified verdict + witness.Design only — no code or runtime changes. Builds on the now-merged #24 proof work and on
docs/Echo-Decomposition.adoc.trope-checker,trope-particularity-workbench, andecho-typesare referenced by URL only (never vendored).The correspondence (the substance)
Both systems already sit on the
echo-typesgraded-loss substrate; this makes that lineage operational.echo_to_residueisdetach— not an analogy.Echo → EchoRisTrope → FloatingQuality;echo_inputis illegal on a residue precisely because aFloatingQualitynode has nobearerfield to project. The[Stab-Erase]once-only debit =detach'sSevered(irrecoverable) loss.GlobalState/RaceConditionlower to the deceptiveConflatedbottom (an untagged merge of particulars) → rejected as a lowering fault underprevent. "Do not silently merge particulars" = Error-Lang's "decomposition must be visible."max(0, 100+Σ)→floor(U) ⊑ acc(output)plus a witness edge ("the operation to repair") — the same invariant-path argminsrc/abi/Stability.idralready reasons about.Honest scope (O2 is ours)
The checker proves grade composition sound; it does not certify that an Error-Lang construct lowered to
detachis adetach. The doc enumerates four per-front-end lowering-correctness obligations —L-Echo/L-Grade/L-Silent/L-Floor— to be discharged with the same Idris2 discipline assrc/abi/. A schema-valid worked IR document (echo_to_residueas adetach) is included.Phasing
Echo/EchoR/echo_to_residuelower cleanly — no new runtime coupling.tropelowering backend (Echo ops first),stabilityFactor → grade+use_model, then the O2 proofs (CI-gated).🤖 Generated with Claude Code
https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Generated by Claude Code